Problem:
v(s(x1)) -> s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
w(s(x1)) -> s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
w(0(x1)) -> p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
p(p(s(x1))) -> p(x1)
p(s(x1)) -> x1
p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(x1))))))))))
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {5,4,3}
transitions:
01(70) -> 71*
01(150) -> 151*
01(130) -> 131*
s1(80) -> 81*
s1(65) -> 66*
s1(40) -> 41*
s1(147) -> 148*
s1(132) -> 133*
s1(92) -> 93*
s1(72) -> 73*
s1(67) -> 68*
s1(42) -> 43*
s1(37) -> 38*
s1(32) -> 33*
s1(27) -> 28*
s1(149) -> 150*
s1(144) -> 145*
s1(129) -> 130*
s1(89) -> 90*
s1(84) -> 85*
s1(79) -> 80*
s1(64) -> 65*
s1(39) -> 40*
s1(29) -> 30*
s1(146) -> 147*
s1(141) -> 142*
s1(131) -> 132*
s1(91) -> 92*
s1(71) -> 72*
s1(66) -> 67*
s1(46) -> 47*
s1(41) -> 42*
s1(36) -> 37*
s1(31) -> 32*
s1(148) -> 149*
s1(93) -> 94*
s1(88) -> 89*
s1(78) -> 79*
s1(48) -> 49*
s1(43) -> 44*
s1(38) -> 39*
s1(145) -> 146*
s1(90) -> 91*
s1(85) -> 86*
p1(45) -> 46*
p1(30) -> 31*
p1(142) -> 143*
p1(137) -> 138*
p1(87) -> 88*
p1(82) -> 83*
p1(77) -> 78*
p1(139) -> 140*
p1(134) -> 135*
p1(74) -> 75*
p1(69) -> 70*
p1(44) -> 45*
p1(34) -> 35*
p1(136) -> 137*
p1(86) -> 87*
p1(81) -> 82*
p1(76) -> 77*
p1(138) -> 139*
p1(133) -> 134*
p1(73) -> 74*
p1(68) -> 69*
p1(33) -> 34*
p1(28) -> 29*
p1(140) -> 141*
p1(135) -> 136*
v1(83) -> 84*
w1(35) -> 36*
p2(202) -> 203*
p2(197) -> 198*
p2(192) -> 193*
p2(172) -> 173*
p2(162) -> 163*
p2(269) -> 270*
p2(239) -> 240*
p2(214) -> 215*
p2(199) -> 200*
p2(164) -> 165*
p2(291) -> 292*
p2(186) -> 187*
p2(313) -> 314*
p2(213) -> 214*
p2(203) -> 204*
p2(188) -> 189*
p2(178) -> 179*
p2(335) -> 336*
p2(180) -> 181*
p2(170) -> 171*
p2(357) -> 358*
v0(2) -> 3*
v0(1) -> 3*
02(277) -> 278*
02(247) -> 248*
02(299) -> 300*
02(321) -> 322*
02(343) -> 344*
02(365) -> 366*
s0(2) -> 1*
s0(1) -> 1*
s2(272) -> 273*
s2(242) -> 243*
s2(212) -> 213*
s2(207) -> 208*
s2(364) -> 365*
s2(359) -> 360*
s2(339) -> 340*
s2(334) -> 335*
s2(319) -> 320*
s2(314) -> 315*
s2(294) -> 295*
s2(274) -> 275*
s2(244) -> 245*
s2(209) -> 210*
s2(361) -> 362*
s2(356) -> 357*
s2(341) -> 342*
s2(336) -> 337*
s2(316) -> 317*
s2(296) -> 297*
s2(276) -> 277*
s2(271) -> 272*
s2(246) -> 247*
s2(241) -> 242*
s2(211) -> 212*
s2(206) -> 207*
s2(201) -> 202*
s2(196) -> 197*
s2(363) -> 364*
s2(358) -> 359*
s2(338) -> 339*
s2(318) -> 319*
s2(298) -> 299*
s2(293) -> 294*
s2(273) -> 274*
s2(268) -> 269*
s2(243) -> 244*
s2(238) -> 239*
s2(208) -> 209*
s2(198) -> 199*
s2(360) -> 361*
s2(340) -> 341*
s2(320) -> 321*
s2(315) -> 316*
s2(295) -> 296*
s2(290) -> 291*
s2(275) -> 276*
s2(270) -> 271*
s2(245) -> 246*
s2(240) -> 241*
s2(215) -> 216*
s2(210) -> 211*
s2(205) -> 206*
s2(200) -> 201*
s2(362) -> 363*
s2(342) -> 343*
s2(337) -> 338*
s2(317) -> 318*
s2(312) -> 313*
s2(297) -> 298*
s2(292) -> 293*
p0(2) -> 5*
p0(1) -> 5*
w2(204) -> 205*
w0(2) -> 4*
w0(1) -> 4*
p3(262) -> 263*
p3(260) -> 261*
00(2) -> 2*
00(1) -> 2*
1 -> 5,48
2 -> 5,27
27 -> 165,78,29
28 -> 64*
29 -> 31*
30 -> 144*
31 -> 179*
32 -> 34,178
42 -> 189,46
43 -> 45,188
47 -> 3*
48 -> 165,78,29
49 -> 28*
64 -> 77,164
65 -> 76*
66 -> 173,70
67 -> 69,172
68 -> 129*
71 -> 171*
72 -> 74,170
75 -> 3*
78 -> 196*
79 -> 187*
80 -> 82,186
84 -> 163*
85 -> 87,162
94 -> 205,36,4
130 -> 238*
131 -> 181,135,192
132 -> 134,180
141 -> 143*
143 -> 205,36,4
151 -> 5*
163 -> 88*
165 -> 78*
171 -> 75*
173 -> 70*
179 -> 35*
181 -> 135*
187 -> 83*
189 -> 46*
193 -> 136*
196 -> 198*
198 -> 200*
200 -> 261*
201 -> 203,260
211 -> 263,215
212 -> 214,262
216 -> 84,163,88
238 -> 240*
247 -> 268*
248 -> 193,136
261 -> 204*
263 -> 215*
268 -> 270*
277 -> 290*
278 -> 137*
290 -> 292*
299 -> 312*
300 -> 138*
312 -> 314*
321 -> 334*
322 -> 139*
334 -> 336*
343 -> 356*
344 -> 140*
356 -> 358*
366 -> 141*
problem:
Qed